Nuprl Lemma : fpf-const_wf
0,22
postcript
pdf
A
,
B
:Type,
L
:
A
List,
v
:
B
.
L
fpf
v
a
:
A
fp
B
latex
Definitions
a
:
A
fp
B
(
a
)
,
L
fpf
v
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
l
member
wf
origin
A, B:Type, L:A List, v:B. L 
fpf
v 
a:A fp B A, B:Type, L:A List, v:B. L fpf v a:A fp B B(a)fpf v l)x:A. B(x) T